<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<html>
	<head>
		<title>Propositions</title>
<link href="../docs-assets/Breadcrumbs.css" rel="stylesheet" rev="stylesheet" type="text/css">
		<meta name="viewport" content="width=device-width initial-scale=1">
		<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
		<meta http-equiv="Content-Language" content="en-gb">

<link href="../docs-assets/Contents.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Progress.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Navigation.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Fonts.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Base.css" rel="stylesheet" rev="stylesheet" type="text/css">
<script>
MathJax = {
	tex: {
		inlineMath: '$', '$'], ['\\(', '\\)'
	},
	svg: {
		fontCache: 'global'
	}
};
</script>
<script type="text/javascript" id="MathJax-script" async
	src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js">
</script>

<script>
function togglePopup(material_id) {
  var popup = document.getElementById(material_id);
  popup.classList.toggle("show");
}
</script>

<link href="../docs-assets/Popups.css" rel="stylesheet" rev="stylesheet" type="text/css">
<link href="../docs-assets/Colours.css" rel="stylesheet" rev="stylesheet" type="text/css">
		
	</head>
	<body class="commentary-font">
		<nav role="navigation">
		<h1><a href="../index.html"><img src="../docs-assets/Inform.png" height=72> </a></h1>
<ul><li><a href="../index.html">home</a></li>
</ul><h2>Compiler</h2><ul>
<li><a href="../structure.html">structure</a></li>
<li><a href="../inbuildn.html">inbuild</a></li>
<li><a href="../inform7n.html">inform7</a></li>
<li><a href="../intern.html">inter</a></li>
<li><a href="../services.html">services</a></li>
<li><a href="../secrets.html">secrets</a></li>
</ul><h2>Other Tools</h2><ul>
<li><a href="../inblorbn.html">inblorb</a></li>
<li><a href="../inform6.html">inform6</a></li>
<li><a href="../inpolicyn.html">inpolicy</a></li>
</ul><h2>Resources</h2><ul>
<li><a href="../extensions.html">extensions</a></li>
<li><a href="../kits.html">kits</a></li>
</ul><h2>Repository</h2><ul>
<li><a href="https://github.com/ganelson/inform"><img src="../docs-assets/github.png" height=0> github</a></li>
</ul><h2>Related Projects</h2><ul>
<li><a href="https://github.com/ganelson/inweb"><img src="../docs-assets/github.png" height=0> inweb</a></li>
<li><a href="https://github.com/ganelson/intest"><img src="../docs-assets/github.png" height=0> intest</a></li>
</ul>
		</nav>
		<main role="main">
		<!-- Weave of 'Propositions' generated by inweb -->
<div class="breadcrumbs">
    <ul class="crumbs"><li><a href="../index.html">Home</a></li><li><a href="../services.html">Services</a></li><li><a href="index.html">calculus</a></li><li><a href="index.html#4">Chapter 4: Propositions</a></li><li><b>Propositions</b></li></ul></div>
<p class="purpose">To build and modify structures representing propositions in predicate calculus.</p>

<ul class="toc"><li><a href="4-prp.html#SP1">&#167;1. Internal representation</a></li><li><a href="4-prp.html#SP4">&#167;4. Walking through propositions</a></li><li><a href="4-prp.html#SP8">&#167;8. Validity</a></li><li><a href="4-prp.html#SP11">&#167;11. Complexity</a></li><li><a href="4-prp.html#SP12">&#167;12. Primitive operations on propositions</a></li><li><a href="4-prp.html#SP17">&#167;17. Inserting and deleting atoms</a></li><li><a href="4-prp.html#SP20">&#167;20. Miscellaneous further operations</a></li><li><a href="4-prp.html#SP21">&#167;21. Inspecting contents</a></li><li><a href="4-prp.html#SP22">&#167;22. Matching sequences of atoms</a></li><li><a href="4-prp.html#SP31">&#167;31. Bracketed groups</a></li></ul><hr class="tocbar">

<p class="commentary firstcommentary"><a id="SP1" class="paragraph-anchor"></a><b>&#167;1. Internal representation.</b>There is no perfectly convenient way to represent propositions. The two
obvious strategies are:
</p>

<ul class="items"><li>(a) Hold them more or less as written, in a flat sequence of atoms.
</li><li>(b) Hold them in a tree which branches at each logical operation.
</li></ul>
<p class="commentary">We follow (a), which is easier to iterate through without tiresome amounts
of recursion, but comes at the cost of extra complexity when it comes to
grouping the terms &mdash; this is why we need the awkward <span class="extract"><span class="extract-syntax">NOT&lt;</span></span> and <span class="extract"><span class="extract-syntax">NOT&gt;</span></span>
atoms, for example. (b) would almost certainly be better if we needed to
accommodate disjunction as well as conjunction, but we do not. The main
demerit of (a) is that it is easy to make malformed propositions, so we have
to build and edit carefully.
</p>

<p class="commentary">So propositions are represented by the <a href="4-ap.html#SP1" class="internal">pcalc_prop</a> object at the front, an
atomic proposition, and this leads via its <span class="extract"><span class="extract-syntax">next</span></span> field to a second atomit
proposition, and so on. Now there's a natural way to store incomplete
propositions and a natural build-point (at the end), and depth-first traverses
are easy &mdash; just work along from left to right.
</p>

<p class="commentary firstcommentary"><a id="SP2" class="paragraph-anchor"></a><b>&#167;2. </b>In particular:
</p>

<ul class="items"><li>(1) The empty list, a <span class="extract"><span class="extract-syntax">NULL</span></span> pointer, represents the universally true
proposition \(\top\). Asserting it does nothing; testing it at run-time always
evaluates to <span class="extract"><span class="extract-syntax">true</span></span>.
</li><li>(2) The conjunction \(\alpha\land\beta\) is almost the concatenation of their
linked lists <span class="extract"><span class="extract-syntax">A --&gt; B</span></span>, except that we must be careful if they appear to have
variables in common.
</li><li>(3) Negation \(\lnot(\phi)\) is the concatenation <span class="extract"><span class="extract-syntax">NOT&lt; --&gt; P --&gt; NOT&gt;</span></span>,
where <span class="extract"><span class="extract-syntax">P</span></span> is the linked list for \(\phi\).
</li><li>(4) The quantifier \(Q v\in \lbrace v\mid\phi(v)\rbrace\) is
<span class="extract"><span class="extract-syntax">QUANTIFIER --&gt; IN&lt; --&gt; P --&gt; IN&gt;</span></span>, where <span class="extract"><span class="extract-syntax">P</span></span> is the linked list for \(\phi\).
</li></ul>
<p class="commentary">Conjunction occurs so densely in propositions arising from
natural language that we save a lot of memory and fuss by simply implying it:
thus "great green dragon" is <span class="extract"><span class="extract-syntax">PREDICATE --&gt; PREDICATE --&gt; PREDICATE</span></span>, rather than
something like <span class="extract"><span class="extract-syntax">PREDICATE --&gt; AND_SIGN --&gt; PREDICATE --&gt; AND_SIGN --&gt; PREDICATE</span></span>.
Disjunction hardly ever occurs, so although the above scheme could simulate
it with \(\alpha\lor\beta = \lnot((\lnot\alpha)\land(\lnot\beta))\), we never do.
</p>

<p class="commentary">The following function determines whether or not <span class="extract"><span class="extract-syntax">P1 --&gt; P2</span></span> should be
understood as a conjunction.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::implied_conjunction_between</span><button class="popup" onclick="togglePopup('usagePopup1')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup1">Usage of <span class="code-font"><span class="function-syntax">Propositions::implied_conjunction_between</span></span>:<br/><a href="4-prp.html#SP3">&#167;3</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p2</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p1</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p2</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p2</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP3" class="paragraph-anchor"></a><b>&#167;3. </b>Purely decoratively, we print some punctuation when logging a proposition;
this is chosen to look like standard mathematical notation.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::debugging_log_text_between</span><button class="popup" onclick="togglePopup('usagePopup2')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup2">Usage of <span class="code-font"><span class="function-syntax">Propositions::debugging_log_text_between</span></span>:<br/><a href="4-prp.html#SP7">&#167;7</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p2</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p1</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p2</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">""</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p2</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">""</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">":"</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p1</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">":"</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP2" class="function-link"><span class="function-syntax">Propositions::implied_conjunction_between</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p1</span><span class="plain-syntax">, </span><span class="identifier-syntax">p2</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">Streams::I6_escapes_enabled</span><span class="plain-syntax">(</span><span class="identifier-syntax">DL</span><span class="plain-syntax">))</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax">(</span><span class="string-syntax">"&amp;"</span><span class="plain-syntax">); </span><span class="comment-syntax"> since </span><span class="extract"><span class="extract-syntax">^</span></span><span class="comment-syntax"> in Inter strings means newline</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> (</span><span class="string-syntax">"^"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="string-syntax">""</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP4" class="paragraph-anchor"></a><b>&#167;4. Walking through propositions.</b>We sometimes need to indicate a position within a proposition &mdash; a position
not of an atom, but between atoms. Consider the possible places where letters
could be inserted into the word "rap": before the "r" (trap), between "r" and
"a" (reap), between "a" and "p" (ramp), after the "p" (rapt). Though "rap" is
a three-letter word, there are four possible insertion points &mdash; so they can't
exactly correspond to letters. The convention we use is that a position marker
points to the //<span class="extract"><span class="extract-syntax">pcalc_prop// structure for the atom before the position
</span></span>meant: and a <span class="extract"><span class="extract-syntax">NULL</span></span> pointer in this context means the front position, before
the opening atom.
</p>

<p class="commentary firstcommentary"><a id="SP5" class="paragraph-anchor"></a><b>&#167;5. </b>The code needed to walk through a proposition is abstracted by the following
macros. Note that we often need to remember the atom before the current one,
so we keep that in a spare variable during each traverse. (This saves us
having to maintain the proposition data structure as a doubly linked list,
which would be harder to edit.)
</p>

<p class="commentary">One macro declares the name of a marker variable to be used when traversing;
the other is the necessary loop head. Note that we do not assume that <span class="extract"><span class="extract-syntax">p</span></span>
will still be non-<span class="extract"><span class="extract-syntax">NULL</span></span> at the end of a loop iteration, just because it
was at the beginning: local edits are sometimes performed in the traverse,
and it can happen that an edit truncates the proposition so savagely that the
loop finds its ground cut out from under it.
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, *</span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="definition-keyword">define</span> <span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">start</span><span class="plain-syntax">)</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">=</span><span class="identifier-syntax">start</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax">=</span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">p</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        (</span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)?(</span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax">=</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">=(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)?(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">):</span><span class="identifier-syntax">NULL</span><span class="plain-syntax">):0, </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)</span>
</pre>
<p class="commentary firstcommentary"><a id="SP6" class="paragraph-anchor"></a><b>&#167;6. </b>An edit which happens during a traverse is permitted to make any change
to the proposition at and beyond the marker position <span class="extract"><span class="extract-syntax">p</span></span>, but not allowed
to change what came before. Since such an edit might leave <span class="extract"><span class="extract-syntax">p</span></span> pointing
to an atom which has been cut, or moved later, we must perform the following
macro after edits to restore <span class="extract"><span class="extract-syntax">p</span></span>. We know that the atom which was before
<span class="extract"><span class="extract-syntax">p</span></span> at the start of the loop has not been changed &mdash; since edits aren't
allowed there &mdash; so <span class="extract"><span class="extract-syntax">p_prev</span></span> must be correct, and we therefore restore
<span class="extract"><span class="extract-syntax">p</span></span> to the next atom after <span class="extract"><span class="extract-syntax">p_prev</span></span>.
</p>

<p class="commentary">There is a catch, however: if our edit consists only of deleting some
atoms then using <span class="extract"><span class="extract-syntax">PROPOSITION_EDITED</span></span> correctly resets <span class="extract"><span class="extract-syntax">p</span></span> to the current
atom at the marker position, and that will be the first atom after the
ones deleted. If we then just go around the loop, we move on to the next
atom; as a result, the first atom after the deleted ones is skipped over.
We can avoid this by using <span class="extract"><span class="extract-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span></span> instead.
</p>

<p class="commentary">Every routine which simplifies a proposition is expected to have an <span class="extract"><span class="extract-syntax">int *</span></span>
argument called <span class="extract"><span class="extract-syntax">changed</span></span>: on exit, the <span class="extract"><span class="extract-syntax">int</span></span> variable this points to
should be set if and only if a change has been made to the proposition.
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_prev</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    *</span><span class="identifier-syntax">changed</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="definition-keyword">define</span> <span class="identifier-syntax">PROPOSITION_EDITED_REPEATING_CURRENT</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">PROPOSITION_EDITED</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">p</span><span class="plain-syntax">##</span><span class="identifier-syntax">_repeat</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
</pre>
<p class="commentary firstcommentary"><a id="SP7" class="paragraph-anchor"></a><b>&#167;7. </b>So we may as well complete the debugging log code now. Note that \(\top\) is
logged as just <span class="extract"><span class="extract-syntax">&lt;&lt; &gt;&gt;</span></span>.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::log</span><button class="popup" onclick="togglePopup('usagePopup3')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup3">Usage of <span class="code-font"><span class="function-syntax">Propositions::log</span></span>:<br/>Calculus Module - <a href="1-cm.html#SP3">&#167;3</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><a href="4-prp.html#SP7" class="function-link"><span class="function-syntax">Propositions::write</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">DL</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
<span class="reserved-syntax">void</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::write</span><span class="plain-syntax">(</span><span class="identifier-syntax">OUTPUT_STREAM</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">"&lt;&lt; "</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="identifier-syntax">bridge</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP3" class="function-link"><span class="function-syntax">Propositions::debugging_log_text_between</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bridge</span><span class="plain-syntax">[0]) </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">"%s "</span><span class="plain-syntax">, </span><span class="identifier-syntax">bridge</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><a href="4-ap.html#SP14" class="function-link"><span class="function-syntax">Atoms::write</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">OUT</span><span class="plain-syntax">, </span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">" "</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">WRITE</span><span class="plain-syntax">(</span><span class="string-syntax">"&gt;&gt;"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP8" class="paragraph-anchor"></a><b>&#167;8. Validity.</b>Since the proposition data structure lets us build all kinds of nonsense,
we'll be much safer if we can check our working &mdash; if we can verify that a
proposition is valid. But what does that mean? We might mean:
</p>

<ul class="items"><li>(i) a proposition is good if its sequence of <span class="extract"><span class="extract-syntax">next</span></span> pointers all correctly
point to <span class="extract"><span class="extract-syntax">pcalc_prop</span></span> structures, and don't loop around into a circle;
</li><li>(ii) a proposition is good if (i) is true, and it is correctly punctuated;
</li><li>(iii) a proposition is good if (ii) is true, and it never confuses
together two different variables by giving both the same letter;
</li><li>(iv) a proposition is good if (iii) is true, and all of its predicates
can safely be applied to all of their terms, and we can identify what
kind of value each variable ranges over.
</li></ul>
<p class="commentary">These are steadily stronger conditions. The first is a basic invariant of
our data structures: nothing failing (i) will ever be allowed to exist,
provided the routines in this section are free of bugs. Condition (ii) is
called syntactic validity; (iii) is well-formedness; (iv) is type safety.
Correct source text eventually makes propositions which have all four
properties, but intermediate half-built states often satisfy only (i).
</p>

<p class="commentary firstcommentary"><a id="SP9" class="paragraph-anchor"></a><b>&#167;9. </b>The following examples illustrate the differences. This one is not even
syntactically valid:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">|</span><span class="identifier-syntax">IN</span><span class="plain-syntax">&lt; --&gt; </span><span class="identifier-syntax">NOT</span><span class="plain-syntax">&gt; --&gt; </span><span class="identifier-syntax">NOT</span><span class="plain-syntax">&gt;|</span>
</pre>
<p class="commentary">This one is syntactically valid, but not well-formed:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">|</span><span class="identifier-syntax">EVERYWHERE</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">) --&gt; </span><span class="identifier-syntax">QUANTIFIER</span><span class="plain-syntax"> </span><span class="identifier-syntax">x</span><span class="plain-syntax"> --&gt; </span><span class="identifier-syntax">PREDICATE</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">)|</span>
</pre>
<p class="commentary">(If <span class="extract"><span class="extract-syntax">x</span></span> ranges over all objects at the middle of the proposition, it had
better not already have a value, but if it doesn't, what can that first
atom mean? It would be like writing the formula \(n + \sum_{n=1}^{10} n^2\),
where clearly two different things have been called \(n\).)
</p>

<p class="commentary">And this proposition is well-formed but not type-safe:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">|</span><span class="identifier-syntax">QUANTIFIER</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">) --&gt; </span><span class="identifier-syntax">kind</span><span class="plain-syntax">=</span><span class="identifier-syntax">number</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">) --&gt; </span><span class="identifier-syntax">EVERYWHERE</span><span class="plain-syntax">(</span><span class="identifier-syntax">x</span><span class="plain-syntax">)|</span>
</pre>
<p class="commentary">(Here <span class="extract"><span class="extract-syntax">x</span></span> is supposed to be a number, and therefore has no location, but
<span class="extract"><span class="extract-syntax">EVERYWHERE</span></span> can validly be applied only to backdrop objects, so what
could <span class="extract"><span class="extract-syntax">EVERYWHERE(x)</span></span> possibly mean?)
</p>

<p class="commentary firstcommentary"><a id="SP10" class="paragraph-anchor"></a><b>&#167;10. </b>The following tests only (ii), validity. <a href="../calculus-test/index.html" class="internal">calculus-test</a> is unable to make
atoms which fail to pass <a href="4-ap.html#SP13" class="internal">Atoms::validate</a>, nor can it make some of the
misconstructions tested for below, but numerous other defects can be tested:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new binary sees (none, none)</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; kind = number (x) ^ even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; sees (4, 10) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (4 == 10) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (x == 10) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (10 == x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (y == x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; NOT&lt; kind = number (x) ^ even (x) NOT&gt; &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; Exists x: even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; NOT&gt; &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - too many close groups</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; Exists x &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; ForAll x &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - nonexistential quantifier without domain</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; ForAll x IN&lt; kind = number (x) IN&gt;: even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; NOT&lt; ^ NOT&gt; ^ NOT&gt; ^ NOT&lt; ^ even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - too many close groups</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; NOT&lt; ^ NOT&lt; ^ even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - 2 group(s) open</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ NOT&lt; ^ even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - group nesting too deep</span>
</pre>
<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">MAX_PROPOSITION_GROUP_NESTING</span><span class="plain-syntax"> </span><span class="constant-syntax">100</span><span class="plain-syntax"> </span><span class="comment-syntax"> vastly more than could realistically be used</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::is_syntactically_valid</span><button class="popup" onclick="togglePopup('usagePopup4')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup4">Usage of <span class="code-font"><span class="function-syntax">Propositions::is_syntactically_valid</span></span>:<br/>Binding and Substitution - <a href="4-bas.html#SP2">&#167;2</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">text_stream</span><span class="plain-syntax"> *</span><span class="identifier-syntax">err</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">groups_stack</span><span class="plain-syntax">[</span><span class="constant-syntax">MAX_PROPOSITION_GROUP_NESTING</span><span class="plain-syntax">], </span><span class="identifier-syntax">group_sp</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="comment-syntax"> (1) each individual atom has to be properly built:</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">char</span><span class="plain-syntax"> *</span><span class="identifier-syntax">v_err</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP13" class="function-link"><span class="function-syntax">Atoms::validate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">v_err</span><span class="plain-syntax">) { </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"atom error: %s"</span><span class="plain-syntax">, </span><span class="identifier-syntax">err</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">        </span><span class="comment-syntax"> (2) every open bracket must be matched by a close bracket of the same kind:</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax"> &gt;= </span><span class="constant-syntax">MAX_PROPOSITION_GROUP_NESTING</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"group nesting too deep"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">groups_stack</span><span class="plain-syntax">[</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax">++] = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax"> &lt;= </span><span class="constant-syntax">0</span><span class="plain-syntax">) { </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"too many close groups"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::counterpart</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">groups_stack</span><span class="plain-syntax">[--</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax">]) != </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"group open/close doesn't match"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="comment-syntax"> (3) every quantifier except "exists" must be followed by domain brackets:</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">)) &amp;&amp; (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> != </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"quantifier without domain"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">        } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"domain without quantifier"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            }</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax">            (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)) &amp;&amp; (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"nonexistential quantifier without domain"</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="comment-syntax"> (4) a proposition must end with all its brackets closed:</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">group_sp</span><span class="plain-syntax"> != </span><span class="constant-syntax">0</span><span class="plain-syntax">) { </span><span class="identifier-syntax">WRITE_TO</span><span class="plain-syntax">(</span><span class="identifier-syntax">err</span><span class="plain-syntax">, </span><span class="string-syntax">"%d group(s) open"</span><span class="plain-syntax">, </span><span class="identifier-syntax">group_sp</span><span class="plain-syntax">); </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP11" class="paragraph-anchor"></a><b>&#167;11. Complexity.</b>Simple propositions contain only unary predicates or assertions that the
free variable has a given kind, or a given value. For example, "a closed
lockable door" is a simple proposition, but "four women in a lighted room"
is complex. The only simple binary predicate is one which assigns a definite
value to <span class="extract"><span class="extract-syntax">x</span></span>. Examples:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new binary sees (none, none)</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; even (x) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; kind = number (x) ^ even (x) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; sees (4, 10) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (4 == 10) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (x == 10) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (10 == x) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (y == x) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; not&lt; kind = number (x) ^ even (x) not&gt; &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; Exists x: even (x) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; Forall x IN&lt; kind = number (x) IN&gt;: even (x) &gt;&gt; is complex</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::is_complex</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">2</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (!(((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">constant</span><span class="plain-syntax">)) ||</span>
<span class="plain-syntax">                ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">constant</span><span class="plain-syntax">)))) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP12" class="paragraph-anchor"></a><b>&#167;12. Primitive operations on propositions.</b>Now for some basic operations, as shown in the following examples:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; NOT&gt; &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - too many close groups</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; Exists x &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; ForAll x &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> false - nonexistential quantifier without domain</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; ForAll x IN&lt; kind = number (x) IN&gt;: even (x) &gt;&gt; is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">set A to &lt;&lt; Exists x &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> a set to &lt;&lt; Exists x &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">set B to &lt;&lt; Exists x: even (x) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> b set to &lt;&lt; Exists x : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">A concatenate B</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; Exists x : Exists x : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">A conjoin B</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; Exists x : Exists y : even(y) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">A concatenate B is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">A conjoin B is syntactically valid</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">A concatenate B is well-formed</span><span class="plain-syntax">':</span><span class="string-syntax"> false - x used outside its binding</span>
<span class="plain-syntax">'</span><span class="element-syntax">A conjoin B is well-formed</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">set P to &lt;&lt; Forall x IN&lt; kind = number (x) IN&gt;: even (x) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> p set to &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">copy of P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">negation of P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; NOT&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) NOT&gt; &gt;&gt;</span>
</pre>
<p class="commentary">Note that the conjunction of A and B renamed the variable <span class="extract"><span class="extract-syntax">x</span></span> in B to <span class="extract"><span class="extract-syntax">y</span></span>,
so that it no longer clashed with the meaning of <span class="extract"><span class="extract-syntax">x</span></span> in A. The concatenation
did not, simply writing one after the other.
</p>

<p class="commentary firstcommentary"><a id="SP13" class="paragraph-anchor"></a><b>&#167;13. </b>First, copying, which means copying not just the current atom, but all
subsequent ones.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::copy</span><button class="popup" onclick="togglePopup('usagePopup5')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup5">Usage of <span class="code-font"><span class="function-syntax">Propositions::copy</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP9">&#167;9</a>, <a href="5-sc.html#SP9_4">&#167;9.4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">original</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">first</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, *</span><span class="identifier-syntax">last</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">original</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">while</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(0);</span>
<span class="plain-syntax">        *</span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax"> = *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">j</span><span class="plain-syntax">=0; </span><span class="identifier-syntax">j</span><span class="function-syntax">&lt;prop-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax">; </span><span class="identifier-syntax">j</span><span class="plain-syntax">++)</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">] = </span><a href="4-trm.html#SP5" class="function-link"><span class="function-syntax">Terms::copy</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[</span><span class="identifier-syntax">j</span><span class="plain-syntax">]);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">first</span><span class="plain-syntax">) </span><span class="identifier-syntax">last</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">first</span><span class="plain-syntax"> = </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">last</span><span class="plain-syntax"> = </span><span class="identifier-syntax">copied_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">first</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP14" class="paragraph-anchor"></a><b>&#167;14. </b>Now to concatenate propositions. If \(E\) and \(T\) are both syntactically valid,
the result will be, too; but the same is not true of well-formedness, so we
need to be careful in using this.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::concatenate</span><button class="popup" onclick="togglePopup('usagePopup6')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup6">Usage of <span class="code-font"><span class="function-syntax">Propositions::concatenate</span></span>:<br/><a href="4-prp.html#SP15">&#167;15</a>, <a href="4-prp.html#SP16">&#167;16</a><br/>Sentence Conversions - <a href="5-sc.html#SP2_7">&#167;2.7</a>, <a href="5-sc.html#SP9_7">&#167;9.7</a>, <a href="5-sc.html#SP9_8">&#167;9.8</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tail</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">end</span><span class="plain-syntax"> = </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">end</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">tail</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">sc</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">while</span><span class="plain-syntax"> (</span><span class="identifier-syntax">end</span><span class="plain-syntax"> &amp;&amp; (</span><span class="identifier-syntax">end</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">sc</span><span class="plain-syntax">++ == </span><span class="constant-syntax">100000</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"malformed proposition"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">end</span><span class="plain-syntax"> = </span><span class="identifier-syntax">end</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">end</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">tail</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP15" class="paragraph-anchor"></a><b>&#167;15. </b>And here is a version which protects us:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::conjoin</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">tail</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax"> == </span><span class="identifier-syntax">tail</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="named-paragraph-container code-font"><a href="4-prp.html#SP15_1" class="named-paragraph-link"><span class="named-paragraph">Report failure to log</span><span class="named-paragraph-number">15.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"conjoin proposition to a subset of itself"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">tail</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax"> == </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="named-paragraph-container code-font"><a href="4-prp.html#SP15_1" class="named-paragraph-link"><span class="named-paragraph">Report failure to log</span><span class="named-paragraph-number">15.1</span></a></span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"conjoin proposition to a superset of itself"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        }</span>

<span class="plain-syntax">    </span><a href="4-bas.html#SP8" class="function-link"><span class="function-syntax">Binding::renumber_bound</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">tail</span><span class="plain-syntax">, </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, -1);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">, </span><span class="identifier-syntax">tail</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP15_1" class="paragraph-anchor"></a><b>&#167;15.1. </b><span class="named-paragraph-container code-font"><span class="named-paragraph-defn">Report failure to log</span><span class="named-paragraph-number">15.1</span></span><span class="comment-syntax"> =</span>
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Seriously misguided attempt to conjoin propositions:\n"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Existing body: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">existing_body</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOG</span><span class="plain-syntax">(</span><span class="string-syntax">"Tail:          $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">tail</span><span class="plain-syntax">);</span>
</pre>
<ul class="endnotetexts"><li>This code is used in <a href="4-prp.html#SP15">&#167;15</a> (twice).</li></ul>
<p class="commentary firstcommentary"><a id="SP16" class="paragraph-anchor"></a><b>&#167;16. </b>Negation and quantification can be done with these shorthand functions:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::negate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
<span class="plain-syntax">        </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">),</span>
<span class="plain-syntax">            </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
<span class="plain-syntax">                </span><span class="identifier-syntax">prop</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">NEGATION_CLOSE_ATOM</span><span class="plain-syntax">)));</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::quantify</span><span class="plain-syntax">(</span><span class="identifier-syntax">quantifier</span><span class="plain-syntax"> *</span><span class="identifier-syntax">quant</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">v</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">parameter</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">domain</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">Q</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP6" class="function-link"><span class="function-syntax">Atoms::QUANTIFIER_new</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">quant</span><span class="plain-syntax">, </span><span class="identifier-syntax">v</span><span class="plain-syntax">, </span><span class="identifier-syntax">parameter</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP16" class="function-link"><span class="function-syntax">Propositions::quantify_using</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Q</span><span class="plain-syntax">, </span><span class="identifier-syntax">domain</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::quantify_using</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">Q</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">domain</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">domain</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">Q</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">Q</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
<span class="plain-syntax">                </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">),</span>
<span class="plain-syntax">                </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span>
<span class="plain-syntax">                    </span><span class="identifier-syntax">domain</span><span class="plain-syntax">,</span>
<span class="plain-syntax">                    </span><a href="4-ap.html#SP4" class="function-link"><span class="function-syntax">Atoms::new</span></a><span class="plain-syntax">(</span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">))));</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP14" class="function-link"><span class="function-syntax">Propositions::concatenate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Q</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP17" class="paragraph-anchor"></a><b>&#167;17. Inserting and deleting atoms.</b>These operations do what they say, but the result is often syntactically
invalid. Handle with care.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">set P to &lt;&lt; Forall x IN&lt; kind = number (x) IN&gt;: even (x) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> p set to &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">insert &lt;&lt; (1 == 2) &gt;&gt; at 0 in P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ('1' == '2') ^ ForAll x IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">insert &lt;&lt; even (x) &gt;&gt; at 2 in P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ForAll x IN&lt; even(x) ^ kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">delete 0 from P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">delete 4 from P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; &gt;&gt;</span>
</pre>
<p class="commentary firstcommentary"><a id="SP18" class="paragraph-anchor"></a><b>&#167;18. </b>Here we insert an atom at a given position, or at the front if the position
is <span class="extract"><span class="extract-syntax">NULL</span></span>.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::insert_atom</span><button class="popup" onclick="togglePopup('usagePopup7')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup7">Usage of <span class="code-font"><span class="function-syntax">Propositions::insert_atom</span></span>:<br/>Binding and Substitution - <a href="4-bas.html#SP10">&#167;10</a><br/>Simplifications - <a href="5-smp.html#SP2_1">&#167;2.1</a>, <a href="5-smp.html#SP4">&#167;4</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP7">&#167;7</a>, <a href="5-smp.html#SP8">&#167;8</a>, <a href="5-smp.html#SP10_3_2">&#167;10.3.2</a>, <a href="5-smp.html#SP15">&#167;15</a>, <a href="5-smp.html#SP19">&#167;19</a>, <a href="5-smp.html#SP20">&#167;20</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">,</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"inserting atom nowhere"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">position</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">position</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">new_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP19" class="paragraph-anchor"></a><b>&#167;19. </b>And similarly, with the deleted atom the one after the position given:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::delete_atom</span><button class="popup" onclick="togglePopup('usagePopup8')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup8">Usage of <span class="code-font"><span class="function-syntax">Propositions::delete_atom</span></span>:<br/><a href="4-prp.html#SP34">&#167;34</a>, <a href="4-prp.html#SP35">&#167;35</a>, <a href="4-prp.html#SP36">&#167;36</a><br/>Simplifications - <a href="5-smp.html#SP10_3_1">&#167;10.3.1</a>, <a href="5-smp.html#SP10_3_2">&#167;10.3.2</a>, <a href="5-smp.html#SP10_4">&#167;10.4</a>, <a href="5-smp.html#SP14">&#167;14</a>, <a href="5-smp.html#SP15">&#167;15</a>, <a href="5-smp.html#SP17_1">&#167;17.1</a>, <a href="5-smp.html#SP19">&#167;19</a>, <a href="5-smp.html#SP20">&#167;20</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"deleting atom nowhere"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"deleting atom off end"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">position</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">position</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP20" class="paragraph-anchor"></a><b>&#167;20. Miscellaneous further operations.</b>The rest of this section is given over to miscellaneous utility functions:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">'</span><span class="element-syntax">new unary even</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">new binary sees (none, sees-f1)</span><span class="plain-syntax">':</span><span class="string-syntax"> ok</span>
<span class="plain-syntax">'</span><span class="element-syntax">set P to &lt;&lt; Forall x IN&lt; kind = number (x) IN&gt;: even (x) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> p set to &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">copy of P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">set Q to negation of P</span><span class="plain-syntax">':</span><span class="string-syntax"> q set to &lt;&lt; NOT&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) NOT&gt; &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">P is a group</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">Q is a group</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">unnegation of Q</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; : even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">remove universal quantifier from P</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; kind=number(x) ^ even(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">set R to delete 4 from P</span><span class="plain-syntax">':</span><span class="string-syntax"> r set to &lt;&lt; ForAll x IN&lt; kind=number(x) IN&gt; &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">remove close domain from R</span><span class="plain-syntax">':</span><span class="string-syntax"> &lt;&lt; ForAll x IN&lt; kind=number(x) &gt;&gt;</span>
<span class="plain-syntax">'</span><span class="element-syntax">P contains quantifier</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">P contains relation</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (1 == 2) &gt;&gt; contains relation</span><span class="plain-syntax">':</span><span class="string-syntax"> true</span>
<span class="plain-syntax">'</span><span class="element-syntax">&lt;&lt; (1 == 2) ^ even (x) &gt;&gt; contains quantifier</span><span class="plain-syntax">':</span><span class="string-syntax"> false</span>
<span class="plain-syntax">'</span><span class="element-syntax">term first cited in &lt;&lt; even (x) &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> x</span>
<span class="plain-syntax">'</span><span class="element-syntax">term first cited in &lt;&lt; not&lt; sees (56, 2) not&gt; &gt;&gt;</span><span class="plain-syntax">':</span><span class="string-syntax"> '56'</span>
</pre>
<p class="commentary firstcommentary"><a id="SP21" class="paragraph-anchor"></a><b>&#167;21. Inspecting contents.</b>First, we count the number of atoms in a given proposition. This is used by
other parts of Inform as a crude measure of how complicated it is; though in
fact it is not all that crude so long as it is applied to a proposition
which has been simplified.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::length</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">n</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) </span><span class="identifier-syntax">n</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">n</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP22" class="paragraph-anchor"></a><b>&#167;22. Matching sequences of atoms.</b>The following sneakily variable-argument-length function can be used to
detect subsequences within a proposition: say, the sequence
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="identifier-syntax">QUANTIFIER</span><span class="plain-syntax"> --&gt; </span><span class="identifier-syntax">PREDICATE</span><span class="plain-syntax"> --&gt; </span><span class="identifier-syntax">anything</span><span class="plain-syntax"> --&gt; </span><span class="identifier-syntax">PREDICATE</span>
</pre>
<p class="commentary">starting at the current position, which could be tested with:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="function-syntax">Propositions::match</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="constant-syntax">4</span><span class="plain-syntax">,</span>
<span class="plain-syntax">        </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax">        </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax">        </span><span class="constant-syntax">ANY_ATOM_HERE</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax">        </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, &amp;</span><span class="identifier-syntax">pp</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
</pre>
<p class="commentary">As can be seen, each atom is tested with an element number and an optional
pointer; when a successful match is made, the optional pointer is set to
the atom making the match. <span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span> atoms are followed by a third
parameter, which if not <span class="extract"><span class="extract-syntax">NULL</span></span> requires it to be a unary predicate of that
family. (So if the routine returns <span class="extract"><span class="extract-syntax">TRUE</span></span> then we can be certain that <span class="extract"><span class="extract-syntax">pp</span></span>
points to the <span class="extract"><span class="extract-syntax">PREDICATE_ATOM</span></span> at the end of the run of four.) There are
two special pseudo-element-numbers:
</p>

<pre class="definitions code-font"><span class="definition-keyword">define</span> <span class="constant-syntax">ANY_ATOM_HERE</span><span class="plain-syntax"> </span><span class="constant-syntax">0</span><span class="plain-syntax"> </span><span class="comment-syntax"> match any atom, but don't match beyond the end of the proposition</span>
<span class="definition-keyword">define</span> <span class="constant-syntax">END_PROP_HERE</span><span class="plain-syntax"> -1 </span><span class="comment-syntax"> a sentinel meaning "the proposition must end at this point"</span>
</pre>
<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::match</span><button class="popup" onclick="togglePopup('usagePopup9')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup9">Usage of <span class="code-font"><span class="function-syntax">Propositions::match</span></span>:<br/><a href="4-prp.html#SP35">&#167;35</a><br/>Sentence Conversions - <a href="5-sc.html#SP9_4">&#167;9.4</a><br/>Simplifications - <a href="5-smp.html#SP5">&#167;5</a>, <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP7">&#167;7</a>, <a href="5-smp.html#SP10_2">&#167;10.2</a>, <a href="5-smp.html#SP15">&#167;15</a>, <a href="5-smp.html#SP19">&#167;19</a>, <a href="5-smp.html#SP20">&#167;20</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">c</span><span class="plain-syntax">, ...) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">va_list</span><span class="plain-syntax"> </span><span class="identifier-syntax">ap</span><span class="plain-syntax">; </span><span class="comment-syntax"> the variable argument list signified by the dots</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">va_start</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="identifier-syntax">c</span><span class="plain-syntax">); </span><span class="comment-syntax"> macro to begin variable argument processing</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">i</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax"> &lt; </span><span class="identifier-syntax">c</span><span class="plain-syntax">; </span><span class="identifier-syntax">i</span><span class="plain-syntax">++) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">a</span><span class="plain-syntax"> = </span><span class="identifier-syntax">va_arg</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">atom_p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">va_arg</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> **);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">atom_p</span><span class="plain-syntax"> != </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) *</span><span class="identifier-syntax">atom_p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">req_up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">a</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) </span><span class="identifier-syntax">req_up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">va_arg</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">a</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">ANY_ATOM_HERE:</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">END_PROP_HERE:</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> != </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">default:</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> != </span><span class="identifier-syntax">a</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">req_up</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                        </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> =</span>
<span class="plain-syntax">                            </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">                        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">family</span><span class="plain-syntax"> != </span><span class="identifier-syntax">req_up</span><span class="plain-syntax">) </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                    } </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">outcome</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                }</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">va_end</span><span class="plain-syntax">(</span><span class="identifier-syntax">ap</span><span class="plain-syntax">); </span><span class="comment-syntax"> macro to end variable argument processing</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">outcome</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP23" class="paragraph-anchor"></a><b>&#167;23. </b>Here we run through the proposition looking for either a given element, or
a given arity, or both:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::prop_seek_atom</span><button class="popup" onclick="togglePopup('usagePopup10')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup10">Usage of <span class="code-font"><span class="function-syntax">Propositions::prop_seek_atom</span></span>:<br/><a href="4-prp.html#SP24">&#167;24</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">atom_req</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">arity_req</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (((</span><span class="identifier-syntax">atom_req</span><span class="plain-syntax"> &lt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">atom_req</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax">            ((</span><span class="identifier-syntax">arity_req</span><span class="plain-syntax"> &lt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="identifier-syntax">arity_req</span><span class="plain-syntax">)))</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::prop_seek_up_family</span><button class="popup" onclick="togglePopup('usagePopup11')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup11">Usage of <span class="code-font"><span class="function-syntax">Propositions::prop_seek_up_family</span></span>:<br/><a href="4-prp.html#SP24">&#167;24</a>, <a href="4-prp.html#SP25">&#167;25</a>, <a href="4-prp.html#SP30">&#167;30</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">up_family</span><span class="plain-syntax"> *</span><span class="identifier-syntax">f</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">f</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP24" class="paragraph-anchor"></a><b>&#167;24. </b>Seeking different kinds of atom is now easy:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::contains_binary_predicate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">2</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::contains_quantifier</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, -1)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">; </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::composited_kind</span><button class="popup" onclick="togglePopup('usagePopup12')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup12">Usage of <span class="code-font"><span class="function-syntax">Propositions::composited_kind</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_7_1">&#167;2.7.1</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-kp.html#SP4" class="function-link"><span class="function-syntax">KindPredicates::is_composited_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">) </span><span class="identifier-syntax">k_atom</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">k_atom</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::contains_nonexistence_quantifier</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">while</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, </span><span class="constant-syntax">1</span><span class="plain-syntax">)) != </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">quantifier</span><span class="plain-syntax"> *</span><span class="identifier-syntax">quant</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">quant</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">quant</span><span class="plain-syntax"> != </span><span class="identifier-syntax">exists_quantifier</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP25" class="paragraph-anchor"></a><b>&#167;25. </b>Here we try to find out the kind of value of variable 0 without the full
expense of typechecking the proposition:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::describes_kind</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">while</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">kind_up_family</span><span class="plain-syntax">)) != </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0])) == </span><span class="constant-syntax">0</span><span class="plain-syntax">)</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="identifier-syntax">val</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP26" class="function-link"><span class="function-syntax">Propositions::describes_value</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">val</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">VALUE_TO_KIND_FUNCTION</span><span class="plain-syntax">(</span><span class="identifier-syntax">val</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP26" class="paragraph-anchor"></a><b>&#167;26. </b>And, similarly, the actual value it must have:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="identifier-syntax">parse_node</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::describes_value</span><button class="popup" onclick="togglePopup('usagePopup13')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup13">Usage of <span class="code-font"><span class="function-syntax">Propositions::describes_value</span></span>:<br/><a href="4-prp.html#SP25">&#167;25</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">switch</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEGATION_OPEN_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</span><span class="plain-syntax">++; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">NEGATION_CLOSE_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</span><span class="plain-syntax">--; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">DOMAIN_OPEN_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</span><span class="plain-syntax">++; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">case</span><span class="plain-syntax"> </span><span class="identifier-syntax">DOMAIN_CLOSE_ATOM:</span><span class="plain-syntax"> </span><span class="identifier-syntax">bl</span><span class="plain-syntax">--; </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">default:</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">bl</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">                    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP10" class="function-link"><span class="function-syntax">Atoms::is_equality_predicate</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">                        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">constant</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">constant</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[1].</span><span class="element-syntax">variable</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">constant</span><span class="plain-syntax">))</span>
<span class="plain-syntax">                            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0].</span><span class="element-syntax">constant</span><span class="plain-syntax">;</span>
<span class="plain-syntax">                    }</span>
<span class="plain-syntax">                }</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">break</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP27" class="paragraph-anchor"></a><b>&#167;27. </b>Finding an adjective is easy: it's a predicate of arity 1.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::contains_adjective</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">)</span>
<span class="plain-syntax">                </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::count_adjectives</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">ac</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">for</span><span class="plain-syntax"> (</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax">; </span><span class="identifier-syntax">p</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">) &amp;&amp;</span>
<span class="plain-syntax">            (</span><a href="4-trm.html#SP8" class="function-link"><span class="function-syntax">Terms::variable_underlying</span></a><span class="plain-syntax">(&amp;(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0])) == </span><span class="constant-syntax">0</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">) </span><span class="identifier-syntax">ac</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">ac</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
</pre>
<p class="commentary firstcommentary"><a id="SP28" class="paragraph-anchor"></a><b>&#167;28. </b>The following searches not for an atom, but for the lexically earliest
term in the proposition:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::get_first_cited_term</span><button class="popup" onclick="togglePopup('usagePopup14')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup14">Usage of <span class="code-font"><span class="function-syntax">Propositions::get_first_cited_term</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP9_4">&#167;9.4</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> &gt; </span><span class="constant-syntax">0</span><span class="plain-syntax">)</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">terms</span><span class="plain-syntax">[0];</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"Propositions::get_first_cited_term on termless proposition"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><span class="plain-syntax">(0); </span><span class="comment-syntax"> never executed, but needed to prevent </span><span class="extract"><span class="extract-syntax">gcc</span></span><span class="comment-syntax"> warnings</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP29" class="paragraph-anchor"></a><b>&#167;29. </b>Here we attempt, if possible, to read a proposition as being either
{\it adjective}(\(v\)) or \(\exists v: {\it adjective}(v)\), where the adjective
can be also be read as a noun, and if so we return a constant term \(t\) for
that noun; or if the proposition isn't in that form, we return \(t=x\), that
is, variable 0.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
<span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::convert_adj_to_noun</span><button class="popup" onclick="togglePopup('usagePopup15')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup15">Usage of <span class="code-font"><span class="function-syntax">Propositions::convert_adj_to_noun</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP9_6">&#167;9.6</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_term</span><span class="plain-syntax"> </span><span class="identifier-syntax">pct</span><span class="plain-syntax"> = </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_variable</span></a><span class="plain-syntax">(0);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">pct</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_existence_quantifier</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)) </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">pct</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> != </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">pct</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">PREDICATE_ATOM</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">arity</span><span class="plain-syntax"> == </span><span class="constant-syntax">1</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="identifier-syntax">up</span><span class="plain-syntax"> = </span><span class="identifier-syntax">RETRIEVE_POINTER_unary_predicate</span><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">predicate</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">up</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">family</span><span class="plain-syntax"> == </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">)</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-trm.html#SP9" class="function-link"><span class="function-syntax">Terms::adj_to_noun_conversion</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">up</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::is_kind_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">kind</span><span class="plain-syntax"> *</span><span class="identifier-syntax">K</span><span class="plain-syntax"> = </span><a href="2-kp.html#SP3" class="function-link"><span class="function-syntax">KindPredicates::get_kind</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">property</span><span class="plain-syntax"> *</span><span class="identifier-syntax">pname</span><span class="plain-syntax"> = </span><span class="identifier-syntax">Properties::property_with_same_name_as</span><span class="plain-syntax">(</span><span class="identifier-syntax">K</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">pname</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-trm.html#SP4" class="function-link"><span class="function-syntax">Terms::new_constant</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">Rvalues::from_property</span><span class="plain-syntax">(</span><span class="identifier-syntax">pname</span><span class="plain-syntax">));</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">pct</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
</pre>
<p class="commentary firstcommentary"><a id="SP30" class="paragraph-anchor"></a><b>&#167;30. </b>We often form propositions which are really lists of adjectives, and the
following are useful for looping through them:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">#</span><span class="identifier-syntax">ifdef</span><span class="plain-syntax"> </span><span class="identifier-syntax">CORE_MODULE</span>
<span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::first_unary_predicate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">ppp</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">ppp</span><span class="plain-syntax">) *</span><span class="identifier-syntax">ppp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-ap.html#SP9" class="function-link"><span class="function-syntax">Atoms::to_adjectival_usage</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>

<span class="reserved-syntax">unary_predicate</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::next_unary_predicate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">ppp</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">ppp</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"bad ppp"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP23" class="function-link"><span class="function-syntax">Propositions::prop_seek_up_family</span></a><span class="plain-syntax">((*</span><span class="identifier-syntax">ppp</span><span class="plain-syntax">)-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">, </span><span class="identifier-syntax">adjectival_up_family</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    *</span><span class="identifier-syntax">ppp</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-ap.html#SP9" class="function-link"><span class="function-syntax">Atoms::to_adjectival_usage</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">}</span>
<span class="plain-syntax">#</span><span class="identifier-syntax">endif</span>
</pre>
<p class="commentary firstcommentary"><a id="SP31" class="paragraph-anchor"></a><b>&#167;31. Bracketed groups.</b>The following routine tests whether the entire proposition is a single
bracketed group. For instance:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="plain-syntax">    </span><span class="identifier-syntax">NOT</span><span class="plain-syntax">&lt; --&gt; </span><span class="identifier-syntax">PREDICATE</span><span class="plain-syntax"> --&gt; </span><span class="identifier-syntax">NOT</span><span class="plain-syntax">&gt;</span>
</pre>
<p class="commentary">would qualify. Note that detection succeeds only if the parentheses match,
and that they may be nested.
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="function-syntax">Propositions::is_a_group</span><button class="popup" onclick="togglePopup('usagePopup16')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup16">Usage of <span class="code-font"><span class="function-syntax">Propositions::is_a_group</span></span>:<br/><a href="4-prp.html#SP32">&#167;32</a>, <a href="4-prp.html#SP33">&#167;33</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">governing</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">match</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::counterpart</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">governing</span><span class="plain-syntax">), </span><span class="identifier-syntax">level</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">match</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"Propositions::is_a_group called on unmatchable"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> != </span><span class="identifier-syntax">governing</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_opener</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">level</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::is_closer</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">)) </span><span class="identifier-syntax">level</span><span class="plain-syntax">--;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">match</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">level</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">)) </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP32" class="paragraph-anchor"></a><b>&#167;32. </b>The following removes matched parentheses, leaving just the interior:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::remove_topmost_group</span><button class="popup" onclick="togglePopup('usagePopup17')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup17">Usage of <span class="code-font"><span class="function-syntax">Propositions::remove_topmost_group</span></span>:<br/><a href="4-prp.html#SP33">&#167;33</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">prop</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) || (</span><a href="4-prp.html#SP31" class="function-link"><span class="function-syntax">Propositions::is_a_group</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">) == </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to remove topmost group which wasn't there"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"ungrouping proposition: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">)) { </span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> = </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">; </span><span class="reserved-syntax">break</span><span class="plain-syntax">; }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"to ungrouped result: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP33" class="paragraph-anchor"></a><b>&#167;33. </b>The main application of which is to remove negation:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::unnegate</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><a href="4-prp.html#SP31" class="function-link"><span class="function-syntax">Propositions::is_a_group</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">NEGATION_OPEN_ATOM</span><span class="plain-syntax">))</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP32" class="function-link"><span class="function-syntax">Propositions::remove_topmost_group</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP34" class="paragraph-anchor"></a><b>&#167;34. </b>More ambitiously, this removes matched parentheses found at any given
point in a proposition (which can continue after the close bracket).
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::ungroup_after</span><button class="popup" onclick="togglePopup('usagePopup18')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup18">Usage of <span class="code-font"><span class="function-syntax">Propositions::ungroup_after</span></span>:<br/><a href="4-prp.html#SP35">&#167;35</a><br/>Simplifications - <a href="5-smp.html#SP6">&#167;6</a>, <a href="5-smp.html#SP15">&#167;15</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">position</span><span class="plain-syntax">, </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> **</span><span class="identifier-syntax">last</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">from</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">int</span><span class="plain-syntax"> </span><span class="identifier-syntax">opener</span><span class="plain-syntax">, </span><span class="identifier-syntax">closer</span><span class="plain-syntax">, </span><span class="identifier-syntax">level</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"removing frontmost group from proposition: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">position</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) </span><span class="identifier-syntax">from</span><span class="plain-syntax"> = </span><span class="identifier-syntax">prop</span><span class="plain-syntax">; </span><span class="reserved-syntax">else</span><span class="plain-syntax"> </span><span class="identifier-syntax">from</span><span class="plain-syntax"> = </span><span class="identifier-syntax">position</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">opener</span><span class="plain-syntax"> = </span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">closer</span><span class="plain-syntax"> = </span><a href="4-ap.html#SP3" class="function-link"><span class="function-syntax">Atoms::counterpart</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">opener</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">closer</span><span class="plain-syntax"> == </span><span class="constant-syntax">0</span><span class="plain-syntax">) </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to remove frontmost group which doesn't open"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">from</span><span class="plain-syntax"> = </span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove opening atom</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">from</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">closer</span><span class="plain-syntax">) { </span><span class="comment-syntax"> the special case of an empty group</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">position</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove opening atom</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">goto</span><span class="plain-syntax"> </span><span class="identifier-syntax">Ungrouped</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">level</span><span class="plain-syntax"> = </span><span class="constant-syntax">0</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">from</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">opener</span><span class="plain-syntax">) </span><span class="identifier-syntax">level</span><span class="plain-syntax">++;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="identifier-syntax">closer</span><span class="plain-syntax">) </span><span class="identifier-syntax">level</span><span class="plain-syntax">--;</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">level</span><span class="plain-syntax"> &lt; </span><span class="constant-syntax">0</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">last</span><span class="plain-syntax">) *</span><span class="identifier-syntax">last</span><span class="plain-syntax"> = </span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">); </span><span class="comment-syntax"> remove closing atom</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">goto</span><span class="plain-syntax"> </span><span class="identifier-syntax">Ungrouped</span><span class="plain-syntax">;</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">internal_error</span><span class="plain-syntax">(</span><span class="string-syntax">"tried to remove frontmost group which doesn't close"</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">Ungrouped:</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"to ungrouped result: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP35" class="paragraph-anchor"></a><b>&#167;35. </b>Occasionally we want to strip away a "for all", and since that is always
followed by a domain specification, we must also ungroup this:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::trim_universal_quantifier</span><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><a href="4-ap.html#SP7" class="function-link"><span class="function-syntax">Atoms::is_for_all_x</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">)) &amp;&amp;</span>
<span class="plain-syntax">        (</span><a href="4-prp.html#SP22" class="function-link"><span class="function-syntax">Propositions::match</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="constant-syntax">2</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><span class="constant-syntax">QUANTIFIER_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">,</span>
<span class="plain-syntax">            </span><span class="constant-syntax">DOMAIN_OPEN_ATOM</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">))) {</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP34" class="function-link"><span class="function-syntax">Propositions::ungroup_after</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">prop</span><span class="plain-syntax"> = </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        </span><span class="identifier-syntax">LOGIF</span><span class="plain-syntax">(</span><span class="identifier-syntax">PREDICATE_CALCULUS_WORKINGS</span><span class="plain-syntax">, </span><span class="string-syntax">"Propositions::trim_universal_quantifier: $D\n"</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<p class="commentary firstcommentary"><a id="SP36" class="paragraph-anchor"></a><b>&#167;36. </b>Less ambitiously:
</p>

<pre class="displayed-code all-displayed-code code-font">
<span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="function-syntax">Propositions::remove_final_close_domain</span><button class="popup" onclick="togglePopup('usagePopup19')"><span class="comment-syntax">?</span><span class="popuptext" id="usagePopup19">Usage of <span class="code-font"><span class="function-syntax">Propositions::remove_final_close_domain</span></span>:<br/>Sentence Conversions - <a href="5-sc.html#SP2_7">&#167;2.7</a></span></button><span class="plain-syntax">(</span><span class="reserved-syntax">pcalc_prop</span><span class="plain-syntax"> *</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="reserved-syntax">int</span><span class="plain-syntax"> *</span><span class="identifier-syntax">move_domain</span><span class="plain-syntax">) {</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">move_domain</span><span class="plain-syntax">) *</span><span class="identifier-syntax">move_domain</span><span class="plain-syntax"> = </span><span class="identifier-syntax">FALSE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_VARIABLE</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">);</span>
<span class="plain-syntax">    </span><span class="identifier-syntax">TRAVERSE_PROPOSITION</span><span class="plain-syntax">(</span><span class="identifier-syntax">p</span><span class="plain-syntax">, </span><span class="identifier-syntax">prop</span><span class="plain-syntax">)</span>
<span class="plain-syntax">        </span><span class="reserved-syntax">if</span><span class="plain-syntax"> ((</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">next</span><span class="plain-syntax"> == </span><span class="identifier-syntax">NULL</span><span class="plain-syntax">) &amp;&amp; (</span><span class="identifier-syntax">p</span><span class="plain-syntax">-&gt;</span><span class="element-syntax">element</span><span class="plain-syntax"> == </span><span class="constant-syntax">DOMAIN_CLOSE_ATOM</span><span class="plain-syntax">)) {</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">if</span><span class="plain-syntax"> (</span><span class="identifier-syntax">move_domain</span><span class="plain-syntax">) *</span><span class="identifier-syntax">move_domain</span><span class="plain-syntax"> = </span><span class="identifier-syntax">TRUE</span><span class="plain-syntax">;</span>
<span class="plain-syntax">            </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><a href="4-prp.html#SP19" class="function-link"><span class="function-syntax">Propositions::delete_atom</span></a><span class="plain-syntax">(</span><span class="identifier-syntax">prop</span><span class="plain-syntax">, </span><span class="identifier-syntax">p_prev</span><span class="plain-syntax">);</span>
<span class="plain-syntax">        }</span>
<span class="plain-syntax">    </span><span class="reserved-syntax">return</span><span class="plain-syntax"> </span><span class="identifier-syntax">prop</span><span class="plain-syntax">;</span>
<span class="plain-syntax">}</span>
</pre>
<nav role="progress"><div class="progresscontainer">
    <ul class="progressbar"><li class="progressprev"><a href="4-ap.html">&#10094;</a></li><li class="progresschapter"><a href="P-wtmd.html">P</a></li><li class="progresschapter"><a href="1-cm.html">1</a></li><li class="progresschapter"><a href="2-up.html">2</a></li><li class="progresschapter"><a href="3-bpf.html">3</a></li><li class="progresscurrentchapter">4</li><li class="progresssection"><a href="4-trm.html">trm</a></li><li class="progresssection"><a href="4-ap.html">ap</a></li><li class="progresscurrent">prp</li><li class="progresssection"><a href="4-bas.html">bas</a></li><li class="progresssection"><a href="4-tcp.html">tcp</a></li><li class="progresschapter"><a href="5-sc.html">5</a></li><li class="progressnext"><a href="4-bas.html">&#10095;</a></li></ul></div>
</nav><!-- End of weave -->

		</main>
	</body>
</html>

